Inference at * 
Iof proof for Lemma typed-null-ite:


  x, y:(Top List), b:. null(if b then x else y fi ) = if b then null(x) else null(y) fi  

latex

 by Auto THEN SplitOnConclITE THEN Auto 

latex

 .

Definitions	Unit, P  Q, P & Q, P  Q, , , b, A, b, null(as), x:A. B(x), Top, t  T
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, assert wf, null wf, top wf